[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification ubi-io-inv
enrich
   ubi-io-pre
with
   

   
   
   
   predicates  ubi-io-inv : apebs;
               ubi-io-initial : apebs;
               ubi-io-peb-inv : apeb;
               ubi-io-peb-initial : apeb;
   
   
   
   

   

   axioms inv :  ⊦ ubi-io-inv(apebs) ↔ (∀ n. n < # apebs → ubi-io-peb-inv(apebs[n]));
          used for: ls;
          initial :  ⊦ ubi-io-initial(apebs) ↔ (∀ n. n < # apebs → ubi-io-peb-initial(apebs[n]));
          used for: ls;
          peb-inv
          : ⊦   ubi-io-peb-inv(apeb)
              ↔   # apeb.data = LEB_SIZE
                ∧ (  ¬ apeb.bad
                   →   (apeb.echdr = empty → apeb.vidhdr = empty) ∧ (apeb.echdr ≠ garbage ∧ apeb.vidhdr = empty → apeb.fill = 0)
                     ∧ apeb.fill ≤ LEB_SIZE ∧ is-aligned(apeb.fill, EB_PAGE_SIZE)
                     ∧ subarray(apeb.data, apeb.fill, LEB_SIZE - apeb.fill) = mkempbuf(LEB_SIZE - apeb.fill));
          used for: ls;
          peb-initial :  ⊦ ubi-io-peb-initial(apeb) ↔ ubi-io-peb-inv(apeb) ∧ (¬ apeb.bad → apeb.echdr.valid? ∧ apeb.vidhdr = empty);
          used for: ls;

   

   
end enrich